Tute (Week 5)

1. Most imperative programming languages do not make the \(\mathbf{else}\) clause of an \(\mathbf{if}\) statement mandatory. TinyImp only has the \(\mathbf{if}\) \(\mathbf{then}\) \(\mathbf{else}\) form. How can a stand-alone \(\mathbf{if}\) be encoded in TinyImp?
2. Conversely, how can \(\mathbf{if}\) \(\mathbf{then}\) \(\mathbf{else}\) be encoded using only stand-alone \(\mathbf{if}\) in TinyImp?
3. MinHS doesn't have stand-alone \(\mathbf{if}\), a design decision shared by most functional programming languages. Unlike TinyImp, there's no sensible way of encoding it. Why is it difficult to encode, and why do you think the language has been designed this way?

Consider the following Haskell implementation of an abstract syntax for MinHS.

data Type =
  Bool
  | Int
  | FunTy Type Type -- Type -> Type
    deriving (Show,Eq)

data Expr =
  Num Int
  | Lit Bool
  | If Expr Expr Expr
  | Apply Expr Expr
  | Plus Expr Expr
  | Eq Expr Expr
  | Recfun Type Type (Expr -> Expr -> Expr)
  | Var String -- only used for pretty-printing. Ignore.

Implement a Value type and an evaluator function for this language.

Here is a big step semantics for a simple expression language, consisting of atomic terms \(\mathbf{P}, \mathbf{A}, \mathbf{PP}, \mathbf{AP}\), \(\mathbf{PPAP}\), and a single operator \(+\).

The big step semantics are as follows:

\[ \dfrac{}{\mathbf{P} \Downarrow \mathbf{P}}{\mathrm{Have}_1} \quad\quad \dfrac{}{\mathbf{A} \Downarrow \mathbf{A}}{\mathrm{Have}_2} \] \[ \dfrac{a \Downarrow \mathbf{P} \quad b \Downarrow \mathbf{A} }{a + b \Downarrow \mathbf{AP} }{\mathrm{Uh}_1} \] \[ \dfrac{a \Downarrow \mathbf{P} \quad b \Downarrow \mathbf{P} }{a + b \Downarrow \mathbf{PP} }{\mathrm{Uh}_2} \] \[ \dfrac{a \Downarrow \mathbf{AP} \quad b \Downarrow \mathbf{PP}}{a + b \Downarrow \mathbf{PPAP} }{\mathrm{Uh}_3} \]

Translate this language to an equivalent small-step semantics where all rules are axioms. Use a stack, similarly to the C-Machine, in order to keep track of the current expression under evaluation.